Upcoming Event: Center for Autonomy Seminar

Abstractions for Scalable Verification of AI-enabled Cyber-Physical Systems

Dr. Pavithra Prabhakar, Professor of Computer Science, University of New Mexico

Abstract

AI-based components have become integral to Cyber-Physical Systems (CPS), enabling transformative functionalities across various domains including transportation, energy, and medicine. Specifically, machine learning components are now widely used for perception, control, and decision-making in safety-critical applications, necessitating rigorous verification methods to ensure safe deployment in real-world environments.  In this talk, we present a formal approach for verifying the safety of AI-enabled CPS. We focus on closed-loop systems that integrate dynamical models of physical processes with neural network-based perception and control modules. We explore two verification scenarios: (1) controllers implemented as neural networks, and (2) perception pipelines combining camera models with neural networks. A key challenge in both settings is the scalability of verification algorithms, particularly due to the large size of neural networks and the complexity introduced by image-based perception.  To address these challenges, we propose abstraction techniques that simplify system representations and make verification tractable. Specifically, we introduce two novel data structures: Interval Neural Networks, which provide abstract representations of neural network behaviors, and Interval Images, which serve as abstract symbolic representations of a set of images. We also present novel abstraction-refinement algorithms that efficiently search for small abstractions to prove system safety. Our experimental results demonstrate that these abstraction-refinement algorithms significantly improve scalability and efficiency by quickly identifying small abstractions to prove safety, enabling the analysis of complex, large-scale AI-enabled CPS.  We also discuss verification approaches for evolving neural networks and highlight ongoing work on stability analysis, refinement checking, compositional analysis, and related challenges.

Biography

Pavithra Prabhakar is a Professor in the Department of Computer Science and the Cleve Moler and MathWorks Endowed Chair in Mathematical and Engineering Software at the University of New Mexico. Prior to joining UNM, she was a Professor of Computer Science and the Peggy and Gary Edwards Chair in Engineering at Kansas State University. She earned her Ph.D. in Computer Science and an M.S. in Applied Mathematics from the University of Illinois Urbana–Champaign, followed by a CMI Postdoctoral Fellowship at the California Institute of Technology.  Prabhakar’s research focuses on formal methods for AI-enabled autonomous, cyber-physical, and robotic systems, with applications in aerospace, automotive, and agricultural automation. She has received numerous honors, including a Marie Curie Career Integration Grant from the EU, NSF CAREER Award, ONR Young Investigator Award, NITW Distinguished Young Alumnus Award, Amazon Research Award, CRA Future Leader recognition, and a 2025 Early Career Academic Achievement Alumni Award from UIUC.  More recently, she served as a Program Director at the National Science Foundation (NSF) in the CISE Directorate, where she led a portfolio of over 200 research projects with a total budget exceeding $100 million, spanning Formal Methods, Cyber-Physical Systems, Robotics, and Artificial Intelligence.